x, y:Atom1. x:Atom1>>y  x = y 

latex

Definitions	Atom$n, t  T, s = t, , x:AB(x), b, x:AB(x), x:A. B(x), Type, AtomFree(T;x), P  Q, x:A. B(x), M(a;g;x), P  Q, P & Q, P  Q, x:T>>a, eq_atom$n(x;y), x.A(x)
Lemmas	eq atom wf1, bool wf, assert wf, matters wf